FETCH LISP.AX;
SHOW PROOF;
∀E APPEND X NILL;
EXIT;FETCH LISP.AX;
∧I INDUCTION2[P←λX.X*NILL = X];
∀E NULL X;
∀E APPEND X NILL;
DISTRIB λY.X*NILL = Y 3:#2;
DISTRIB λY.X*NILL = Y, IF NULL X THEN NILL ELSE CONS(CAR X,CDR X*NILL);
DISTRIB IF NULL X THEN NILL ELSE CONS(CAR X,CDR X*NILL),λY.Y = X*NILL;
DISTRIB λX.P(X), IF TRUE THEN X ELSE Y;
DISTRIB λX.CAR(X), IF TRUE THEN X ELSE Y;
EXIT;FETCH LISP.AX;FETCH LISP.AX;
∧I INDUCTION2[P←λX.X*NILL = X]:
∧I INDUCTION2[P←λX.X*NILL = X]:
∧I INDUCTION2[P←λX.X*NILL = X];
∀E APPEND X NILL;FETCH LISP.AX;
∧I INDUCTION2[P←λX.(X*NILL) = X];
∀E APPEND X NILL;
DISTRIB λY.=(Y,X*NILL) 2:#2;
EXIT;fetch lisp.ax;
∧I INDUCTION2[P←λX.X*NIcL = X];
∧I INDUCTION2[P←λX.X*NILL = X];
∀E APPEND X NIL;
∀E APPEND X NILL;
DISTRIB λY.(Y = X*NILL) 2:#2;
DISTRIB λY.=(Y , X*NILL) 2:#2;
TAUT 3:#2≡(NULL X⊃NILL=(X*NILL))∧(¬(NULL X)⊃CONS(CAR X,(CDR X)*NILL)=(X*NILL));
SHOW PROOF;
SHOW PROOF;
EXIT;SHOW PROOF;
∀E NULL X;
CANCEL;
TAUTEQ 4:#2 2 3 4;
CANCEL 3;
SHOW PROOF;
DISTRIB λY.(X*NILL=Y) 2:#2;
DISTRIB λY.=(X*NILL,Y) 2:#2;
SUBST 3 IN 3;
CANCEL;
SUBST 3 IN 2;
CANCEL;
SUBSTR 3 IN 2;
TAUT (NULL X⊃(X*NILL)=NILL)∧(¬NULL X⊃X*NILL=CONS(CAR X,(CDR X)*NILL)) 4;
SHOW PROOF;
∀E NULL X;
TAUTEQ NULL X ⊃ X*NILL = X 5 6;

EXIT;FETCH LIST.AX;FETCH LIST.AX;
∧I INDUCTION[P←λX.X*NILL=X];
∀E APPEND U NILL;
DISTRIB λY.=(U*NILL,Y) 2:#2;
SUBSTR 2 IN 3;
CANCEL;
SUBST 2 IN 3;
CANCEL;
SHOW PROOF;
TAUT 3:#2 2 3;
CANCEL;
TAUT (NULL U⊃(U*NILL)=NILL)∧(¬NULL U⊃(U*NILL)=CONS(CAR U,(CDR U)*NILL)) 2 3;
EXIT;SHOW PROOF;
∀E NULL U;
SHOW AXIOM CONS;
∀E CONS3 U;
SHOW PROOF;
TAUTEQ 1:#1#1 4 5 6;
TAUT NULL U ⊃ U*NILL = U 4 5;
TAUTEQ NULL U ⊃ U*NILL = U 4 5;
TAUTEQ ¬NULL U ∧ (CDR U)*NILL = CDR U ⊃ CONS(CAR U,(CDR U)*NILL) =U 6;
ASSUME (CDR U)*NILL = CDR U;
SHOW PROOF;
SUBST 8 IN 6;
⊃I 8 9;
TAUTEQ 1:#1#1 6 10;
TAUTEQ 1:#1#1 4 6 10;
TAUT 1:#1#1 ⊃ 1:#1#1;
CANCEL;







SHOW PROOF;
TAUTEQ ¬NULL U ∧ (CDR U)*NILL=CDR U ⊃ U*NILL = U 4 10;
TAUTEQ 1:#1#1 7 11;
∀I 12 U;
MP 13 1;
EXIT;SAVE PROOF→APPNIL.PRF;
SHOW PROOF→APPNIL.FETCH LISP.AX;FETCH LIST.AX;
EXIT;